i x(op;id;inv) e == if 0 z i then i x(op;id) e else inv(-i x(op;id) e) fi  

latex

Up	groups 1
Wellformedness Lemmas	int op wf
Definitions	if b then t else f fi , i z j, n x(op;id) e